a, b:. a  b  (a < b  (a = b)) 

latex

Definitions	x,y. t(x;y), , x f y, t  T, OMon, t.1, Mon, x(s1,s2), P & Q, AbMon, OCMon, OGrp, <+>, |g|, x:A. B(x), r < s, r  s
Lemmas	ocgrp wf, grp le wf, assert wf, grp car wf, linorder wf, qadd grp wf2, grp leq iff lt or eq